A category of cubes is a category of geometric shapes for higher structures in which the basic shapes are cubes of all dimensions. There are actually many different categories of cubes, depending on what sorts of operations are permitted between cubes. In general, we expect the following of a category of cubes:
Often one asks that the monoidal structure is strict, in which case any cube category is a PRO. Besides the faces and degeneracies, a cube category might also include
Often we describe a cube category as generated by some subset of these morphisms. Typically there is a functor from to Top sending the -cube to the topological -cube .
A presheaf on a category of cubes is a cubical set.
A uniform way to present many cube categories is as free (strict) monoidal categories with some structure, i.e., as classifying categories for monoidal theories (Mauri 2005). This approach is described by Grandis and Mauri (2003) and expanded upon by Buchholtz and Morehouse (2017). In these descriptions, some morphisms between cubes play the role of structural rules, reflecting additional requirements on the monoidal structure:
Including permutations thus makes the cube category a PROP, while including all structural rules makes it a Lawvere theory. Other morphisms, such as connections or reversals, are instead “operations”.
The construction of the classifying category can be unpacked into an explicit description of a cube category in terms of generating morphisms and relations (the “cubical identities”). Most cube categories can also be described as wide subcategories of the full subcategory of Set consisting of for : a morphism between cubes is determined by its behavior on vertices.
At least in the cartesian case, the classifying category description implies that is equivalent to the opposite of the category of free finitely-generated algebras for the theory. The 1-cube can often be cast as a dualizing object, yielding another description of the cube category.
The ordered cube category or restricted cube category (Grandis & Mauri 2003, Section 4) is the minimal cube category, generated by face and degeneracy maps. When unqualified, cube category usually refers to this category, which historically was the first to be defined.
The ordered cube category is the free strict monoidal category with terminal unit equipped with an object and two maps .
Let be an integer. We denote the object of by .
In addition to the maps and , maps of the form for are also called faces. Finite composites of such maps may also be called faces. Likewise, maps of the form for are also called degeneracies.
See (Grandis & Mauri 2003, Section 4) for the following two propositions.
The ordered cube category is the classifying category of the monoidal theory of bipointed objects with the weakening structural rule.
The ordered cube category is isomorphic to the subcategory of whose objects are powers of , , and whose morphisms are generated by degeneracy maps which delete a coordinate and face maps which insert a 0 or 1 without modifying the order of coordinates. The monoidal product is the restriction of the cartesian product on . The basic face maps are the two inclusions and the basic degeneracy is the map .
It follows from Proposition that every morphism in can be written as a finite composite of maps of the form and . An explicit description of the ordered cube category by generators and relations is in section 2 of
Write for the full subcategory of consisting of and .
The category is isomorphic to the category , i.e. it may also be described as
The full subcategory of the simplex category on the objects and .
(A skeleton of) the category of linearly ordered sets of cardinality 1 or 2.
The indexing category for reflexive equalizers.
itself can be recovered as the free strict monoidal category? on whose unit object is . Note that is not the free strict monoidal category on , but the free strict monoidal category with specified unit on , where the unit is specified to be .
For , an -connection in a cube category is a morphism such that defines a monoid in a monoidal category and additionally the equations
hold. Often these are called negative and positive connections rather than - and -connections respectively. We can think of the negative connection as the morphism of topological spaces sending a pair of points to their maximum, likewise the positive connection as the minimum. We may more generally refer to maps of the form as connections.
The ordered cube category with an -connection is the free strict monoidal category with terminal unit equipped with an object , two maps , and an -connection.
We can also consider the cube category with both negative and positive connections. The cube category has several advantages over the minimal cube category as a shape for higher structures; see connection on a cubical set for more information.
The symmetric cube category is the free strict symmetric monoidal category with terminal unit equipped with an object and two maps .
The symmetric cube category is also called the semicartesian cube category, as well as the “BCH” cube category after its use by Bezem, Coquand, & Huber (2013) to interpret homotopy type theory constructively. It is also used in the semantics of internally parametric dependent type theory.
The symmetric monoidal structure induces an automorphism for each element of the symmetric group on elements. The symmetric cube category can be compared with the symmetric simplex category and cyclic category, which similarly add symmetries to the simplex category. Note that while the symmetric simplex category includes all the natural symmetries of an -simplex, the symmetric cube category only includes the symmetries of the -cube coming from permutations of the axes.
The symmetric cube category admits the following alternative description, used by Bezem, Coquand, and Huber:
The symmetric cube category is equivalent to the category whose objects are finite sets and whose morphisms are set functions such that the restriction of to the preimage of is injective.
A cubical set over the symmetric cube category can also be seen as a nominal set with additional structure; see Pitts (2015).
Isaacson (2011) uses a cube category with symmetries and a positive connection, while Grandis and Mauri (2003) describe a cube category with symmetries and both positive and negative connections. Grandis and Mauri also take the connections to be symmetric, making are commutative monoids for , while Isaacson does not.
A reversal or reversion in a cube category is a involution such that for . Topologically, we think of a reversal as the automorphism of the topological 1-cube sending to .
Grandis and Mauri (2003, Section 9) consider a cube category generated by connections, symmetries, and reversals (on top of faces and degeneracies). They also impose laws governing the interaction between reversals and connections, , which reflect the equations satisfied by the topological , , and reversal.
By adding diagonal morphisms on top of the symmetric cube category, we arrive at the cartesian cube category.
Symmetries can already be derived from the combination of degeneracies and diagonals (Mauri 2005, Corollary 5.5), though not if one only assumes a diagonal .
The cartesian cube category is the free strict cartesian monoidal category equipped with an object and two maps .
The cartesian cube category is thus the Lawvere theory of bi-pointed objects. In particular, it is dual to the category of free finite bi-pointed sets. By a Stone-type duality with as a dualizing object, itself admits an algebraic description:
The cartesian cube category is isomorphic to the subcategory of Set consisting of maps preserving binary and .
Cartesian cube categories (with or without additional structure) are used in the semantics of homotopy type theory and cubical type theory. The use of a cube category with diagonals for this purpose was proposed by Coquand (2014). The first constructed model of this kind used the De Morgan cube category (Cohen, Coquand, Huber & Mörtberg, 2015) (see below), but the construction can be (non-trivially) modified to work for the cartesian cubes of Definition (Angiuli, Brunerie, Coquand, Harper, Favonia & Licata 2021). Various cartesian cube categories are categorized by Buchholtz and Morehouse (2017).
In the cartesian regime, there is a proliferation of options for the laws governing the interaction of operations such as connections or reversals. For example, one may ask that the positive and negative connections distribute over each other, a condition which only makes sense in the presence of diagonals. The following two choices, for one and two connections respectively, reflect the equational theory of the topological -cubes when we interpret diagonals by geometric diagonals and connections by and .
The join (resp. meet) semilattice category is the Lawvere theory of bounded join (resp. meet) semilattices. (The join and meet variants are of course isomorphic.)
The distributive lattice cube category (or Dedekind cube category) is the Lawvere theory of bounded distributive lattices.
Like the cartesian cube category, these have alternate characterizations via Stone-type dualities (and in particular Birkhoff duality) mediated by .
The distributive lattice cube category is isomorphic to the full subcategory of Pos consisting of the powers for . The join semilattice cube category is isomorphic to the wide subcategory thereof consisting of maps preserving binary joins.
Unlike the previously discussed cube categories, the cartesian cube categories with one or more connections are not Cauchy complete. For applications using presheaves on the cube category, it is often convenient to work with their Cauchy completions.
The Cauchy completion of the distributive lattice cube category is equivalent to the full subcategory of Pos consisting of finite (bounded) lattices. The Cauchy completion of the join semilattice cube category is equivalent to the subcategory of Pos consisting of finite (bounded) distributive lattices and morphisms preserving binary joins.
(Sattler 2019) and (Cavallo & Sattler (2022), Theorem 4.46).
There is a fully faithful functor from the simplex category into the Cauchy completions of the semilattice and distributive lattice cube categories, corresponding to the inclusion of linear orders in the categories of Proposition .
Buchholtz and Morehouse (2017) consider the cube categories with symmetries, diagonals, connections, and reversals (on top of faces and degenerecies) given by the Lawvere theories of De Morgan algebras, Kleene algebras, and Boolean algebras, the differences between them being in the equational theory of morphisms.
The Kleene cube category is the choice that makes the evident functor faithful. The De Morgan cube category is used in the model of cubical type theory of Cohen, Coquand, Huber & Mörtberg (2015), but the construction also works with Kleene and Boolean cubes. The Cauchy completion of the Boolean cube category is the category FinSet of nonempty finite sets, so the category of Boolean cubical sets is equivalent to the category of symmetric sets.
Many (perhaps all) of the cube categories described above are test categories (Buchholtz & Morehouse 2017). Hence their categories of cubical sets model homotopy types. Cube categories with connections or diagonals are generally strict test categories, while the ordered and symmetric cube categories are not. See model structure on cubical sets and connection on a cubical set for more details.
Among all geometric shapes for higher structures cubes are best suited for describing Gray-like tensor products of higher structures: there is geometrically obvious way in which to combine the -cube and the -cube to the -cube . The monoidal structure on the ordered cube category induces the canonical monoidal structure on cubical sets and then on strict omega-categories: the Crans-Gray tensor product.
Many (but not all) cube categories can be seen as Reedy categories (or generalized Reedy categories if they contain non-trivial automorphisms), with the degree of an cube given by its dimension. The Reedy face maps are the cubical faces and diagonals (if present), while the Reedy degeneracy maps are the cubical degeneracies and connections (if present).
Those cube categories which are Reedy categories are generally also elegant Reedy categories, or Eilenberg-Zilber categories if they contain automorphisms. Campion (2023) enumerates a collection of cube categories and determines which of them are Eilenberg–Zilber categories.
The cube categories without diagonals (i.e., having possibly symmetries, connections, or reversals on top of faces and degeneracies) are Eilenberg–Zilber categories.
Cube categories with diagonals are more delicate.
The cartesian cube category (of ) is an Eilenberg–Zilber category, as is the cartesian cube category with reversals.
A Reedy category is always Cauchy complete, so for cube categories with diagonals and connections we may need to consider their Cauchy completions.
The Cauchy completion of the semilattice cube category admits no Reedy structure.
The Cauchy completion of the distributive lattice cube category is not an Eilenberg–Zilber category.
(Cavallo & Sattler 2022) develops a generalization of the theory of EZ-categories which can be used to work with the semilattice cube category, but this theory does not apply to the distributive lattice cube category (Cavallo & Sattler 2022, Appendix A.2).
The Cauchy completion of the Boolean cube category is an Eilenberg–Zilber category.
See also the related entries at cubical set.
Zoologies of cube categories:
Marco Grandis and Luca Mauri, Cubical sets and their site, Theory Applic. Categories 11 (2003) 185–201 [tac]
Ulrik Buchholtz, Edward Morehouse, Varieties of Cubical Sets, Relational and Algebraic Methods in Computer Science (RAMICS 2017), Lecture Notes in Computer Science 10226 (2017) 77–92 [arXiv:1701.08189, doi:10.1007/978-3-319-57418-9_5]
For the semicartesian cube category:
Marc Bezem, Thierry Coquand, Simon Huber, A Model of Type Theory in Cubical Sets, 19th International Conference on Types for Proofs and Programs (TYPES 2013). (doi:10.4230/LIPIcs.TYPES.2013.107)
Andrew Pitts, Nominal Presentation of Cubical Sets Models of Type Theory, Proceedings of the 20th International Conference on Types for Proofs and Programs (TYPES 2014). (doi:10.4230/LIPIcs.TYPES.2014.202)
Mike Shulman, Towards a Third-Generation HOTT Part 3 (slides, video)
Cubes with symmetries and a connection:
Cubes with diagonals:
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata, Syntax and models of Cartesian cubical type theory, Mathematical Structures in Computer Science 31(4) (2021). (doi:10.1017/S0960129521000347)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom, 21st International Conference on Types for Proofs and Programs (TYPES) (2015). (doi:10.4230/LIPIcs.TYPES.2015.5, arXiv:1611.02108)
Thierry Coquand, Variation on Cubical sets (2014) [pdf]
Christian Sattler, Idempotent completion of cubes in posets (2019) [arXiv:1805.04126]
Evan Cavallo and Christian Sattler, Relative elegance and cartesian cubes with one connection (2022). [arXiv:2211.14801]
On Eilenberg–Zilber structures:
Last revised on January 6, 2025 at 14:54:46. See the history of this page for a list of all contributions to it.